\begin{tabbing}
EOrderAxioms\=\{i:l\}\+
\\[0ex]($E$; ${\it pred?}$; ${\it info}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:$E$, $l$:IdLnk.\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex]($\forall$${\it e''}$:$E$. 
\\[0ex]($\uparrow$rcv?(${\it info}$;${\it e''}$))
\\[0ex]$\Rightarrow$ (sender(${\it info}$;${\it e''}$) = $e$ $\in$ $E$)
\\[0ex]$\Rightarrow$ (link(${\it info}$;${\it e''}$) = $l$ $\in$ IdLnk)
\\[0ex]$\Rightarrow$ \=(((${\it e''}$ = ${\it e'}$ $\in$ $E$) $\vee$ cless($E$;${\it pred?}$;${\it info}$;${\it e''}$;${\it e'}$))\+
\\[0ex]$\wedge$ (loc(${\it info}$;${\it e'}$) = destination($l$) $\in$ Id))))
\-\-\\[0ex]$\wedge$ \=($\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex](loc(${\it info}$;$e$) = loc(${\it info}$;${\it e'}$) $\in$ Id)
\\[0ex]$\Rightarrow$ (${\it pred?}$($e$) = ${\it pred?}$(${\it e'}$) $\in$ ($E$ + Unit))
\\[0ex]$\Rightarrow$ ($e$ = ${\it e'}$ $\in$ $E$))
\-\\[0ex]$\wedge$ strongwellfounded($E$; $e$,${\it e'}$.pred!($E$;${\it pred?}$;${\it info}$;$e$;${\it e'}$))
\\[0ex]$\wedge$ ($\forall$$e$:$E$. ($\neg$($\uparrow$first(${\it pred?}$;$e$))) $\Rightarrow$ (loc(${\it info}$;pred(${\it pred?}$;$e$)) = loc(${\it info}$;$e$) $\in$ Id))
\\[0ex]$\wedge$ ($\forall$$e$:$E$. ($\uparrow$rcv?(${\it info}$;$e$)) $\Rightarrow$ (loc(${\it info}$;sender(${\it info}$;$e$)) = source(link(${\it info}$;$e$)) $\in$ Id))
\\[0ex]$\wedge$ \=($\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex]($\uparrow$rcv?(${\it info}$;$e$))
\\[0ex]$\Rightarrow$ ($\uparrow$rcv?(${\it info}$;${\it e'}$))
\\[0ex]$\Rightarrow$ (link(${\it info}$;$e$) = link(${\it info}$;${\it e'}$) $\in$ IdLnk)
\\[0ex]$\Rightarrow$ cless($E$;${\it pred?}$;${\it info}$;sender(${\it info}$;$e$);sender(${\it info}$;${\it e'}$))
\\[0ex]$\Rightarrow$ cless($E$;${\it pred?}$;${\it info}$;$e$;${\it e'}$))
\-\-
\end{tabbing}